$\forall$$E$, $T$:Type, $x$:$E$. tree\_leaf($x$) $\in$ tree\_con($E$;$T$)